
\documentclass[runningheads]{llncs}
\hyphenation{evaluation}
\lefthyphenmin = 3
\righthyphenmin=4

\usepackage{amsmath}
\usepackage{txfonts}
\usepackage{stmaryrd}
\usepackage{amsfonts}

\usepackage{amssymb}
\setcounter{tocdepth}{3}
\usepackage{graphicx}
\usepackage{algorithmic, algorithm}

\usepackage{url}
\newcommand{\keywords}[1]{\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}

\begin{document}

\mainmatter  % start of an individual contribution

% first the title is needed
\title{A Refinement Methodology for Formal PLC Verification}

% a short form should be given in case it is too long for the running head
\titlerunning{}

% the name(s) of the author(s) follow(s) next
%
% NB: Chinese authors should write their first names(s) in front of
% their surnames. This ensures that the names appear correctly in
% the running heads and the author index.
%
\author{Hai Wan, Gang Chen, Xiaoyu Song, Ming Gu}
%
\authorrunning{}
% (feature abused for this document to repeat the title also on left hand pages)

% the affiliations are given next; don't give your e-mail address
% unless you accept that it will be published
\institute{}

\toctitle{} \tocauthor{} \maketitle


\begin{abstract}
Programmable logic controllers (PLCs) are widely used in embedded systems. A timer plays a pivotal
role in PLC real-time applications. In our previous work, a formalization of PLC programs with
TON-timers was presented in the theorem proving system Coq. The behavior of a timer was
characterized by a set of axioms at an abstract level. Two key points of the work were the abstract
model and its interpretation. In this paper, we extend our previous work. Firstly, a concrete model
is built and the correctness of the abstract model is proved based on the concrete model. Secondly,
the interpretation is generalized by the introduction of a mapping function. Both works are done in
a unified framework that we propose in the paper. The essence of the framework is the notion of
refinement relation. We also give the principles of the correctness proof. As a case study, we
reconsider the quiz machine program. The experiment result shows the correctness of the framework.

\keywords{PLC, real-time systems, theorem proving, Coq, TON-timer, translation validation,
refinement relation}
\end{abstract}

\section{Introduction}

Programmable logic controllers (PLCs) are widely used for safety critical applications in various
industrial fields. The correctness and reliability of PLC programs are of great importance. Two
distinguished features of PLCs programs are the use of timers and the cyclic behavior. In our
previous work \cite{cg_Coq_PLCII}, we formally modeled and proved the correctness of a PLC program
with timer control. Timers are explicitly modeled by a set of axioms. The behavior of the model is
represented by a set of sequences (or traces) where a sequence is an ordered list of systems
states. Our model is at the scan cycle level, which means that each state in the sequence is a
snapshot in a scan cycle. Comparing to the rung level model (i.e., each rung is represented by a
state in the sequence), the model we used is an abstract model. We discussed how to map the states
in the scan cycle level sequence to those in the rung level sequence. There are several mappings.
According to the rung level model, the correctness of the abstract model was proved manually
without a formal Coq proof. In this paper, we continue our work. Firstly the idea of mapping is
generalized. Secondly the correctness of the abstract model is formally proved in Coq. These two
issues are solved in a unified framework whose essence is the notion of refinement relation.
Mapping and property preservation are key components and properties of refinement relation.

Translation validation \cite{Pnueli98translationvalidation} is an approach to the verification of
translators. It is deployed to check whether the generated code is a correct implementation of the
source code. In this paper we adopt this approach to prove the correctness of the abstract model.
In order to establish the refinement relation between two models, first a common semantic framework
for the representations of models is needed; second, a formal definition of refinement relation
should be defined based on the semantic framework. Because of the real-time nature and time related
properties of PLC programs, we adopt an extension of the semantic framework of
 \cite{Pnueli98translationvalidation} with the expressive power to represent time.
We use timed execution sequences \cite{TPM_TTS} as the common semantic base for the concrete and
abstract models. The behavior of the concrete (or abstract) model is modeled by a set of timed
execution sequences. The notion of refinement is then defined as a relation among sequences from
the two sets.

Our computational model which is call timed STS is an extension of synchronous transition system
(STS) \cite{Pnueli98translationvalidation}. A timed STS consists of two parts: an STS and
additional predicates describing the behavior of timers \cite{cg_Coq_PLCII}. Concrete and abstract
models are built at different abstract levels. In each model, PLC timers are modeled explicitly.
Based on the structure of the model, instead of verifying all timed state sequences to show the
refinement relation (which is formally defined in section \ref{comp_model_refinement_relation}), it
is enough to prove that there exists a refinement relation between the synchronous transition
systems and a refinement relation between the additional predicates. For the transition systems
part, the refinement relation can be checked by a model checker or an automatic theorem prover. For
the time related part, by adding several constraints to the PLC program, there is always a
refinement relation. These constraints are reasonable and well accepted by PLC programmers.

The rest of the paper is organized as follows. In section \ref{related_work} we summarize the
related works. Section \ref{PLC_TIMERS} introduces PLC and its timers and an illustrative example.
The formal definitions of the computational model and refinement relation is given in section
\ref{comp_model_refinement_relation}. The principles of modeling PLC programs with timers as well
as the outline of how to prove the refinement relation are described in detail in section
\ref{modeling_PLC_with_Timers}. Finally section \ref{conclusion} concludes the paper.

\subsection{Related Works}
\label{related_work}

On the modeling and verification of PLC programs, the methods used can be divided into two main
directions: model checking and theorem proving. Timed automata are used to model PLC programs
\cite{Mader99timedautomaton} \cite{ProvingSequentialFunctionChartProgramsUsingAutomata}. In
\cite{dierks01plcautomata} Structured Text programs are automatically generated from PLC-automata.
They didn't model PLC programs with timers, but use timers to implement PLC-automata.
Condition/event systems are also adopted to model PLC programs \cite{NBauer:Thesis:1998}. In
\cite{ModellingPLCLV} the Ladder Diagram programs are researched and time is treated implicitly.
Model checker SMV was used to verify the model. In \cite{SynSignalModelPLC}, the synchronous
language SIGNAL is used to model Structured Text and Function Block Diagram programs. They did not
treat timers. In \cite{DBLP:journals/rts/KramerV97} theorem prover Isabelle/HOL system was used to
model and verify PLC programs. Module verification method is adopted in the paper. They had a
simple model of time, because they assumed the the current value increases monotonously and there
is no reset action during this process. No explicit model of a timer was given.

The translation validation approach is used to ensure the correctness of the generated codes in
\cite{KMR-ppdp2005}. In \cite{TV_in_OPT_COML}, the approach is adopted to compares the intermediate
form of the program before and after each compiler pass and verify the preservation of semantics.
In \cite{DBLP:conf/etfa/PollmacherZH05}, the authors employ translation validation for
code-generators of PLCs. Comparing to their work, our definition of refinement relation is
different in two ways. First they do not have the sampling function. The introduction of sampling
function helps to build a refinement relation between two models and ensure that the cyclic
behavior of PLCs is modeled. Second they have a constraint that the initial states of the abstract
model are mapped to a subset of the initial states of the concrete model. We think this is an
obstacle in proving the correctness of the abstract model, since it may make the abstract sequences
unable to cover all the concrete sequences. Sampling and temporal abstraction are proposed and used
to do hardware verifications \cite{HOLandHardwareVerification}
\cite{AutomaticVericationMicroprecessor} \cite{GenericInterpreter}. An extension of temporal
abstraction is used in the paper because we need to model the behavior of timers, which involve the
explicit treatment of time.

\section{Programmable Logic Controller and Timers}
\label{PLC_TIMERS}
%\begin{figure}[]
%        \center\includegraphics[scale = 0.5]
%        {figs/structure_plc}
%        \caption{\label{structure_plc} PLC cycle}
%      \end{figure}
A PLC system typically consists of a CPU, a memory and input/output points through which the system
communicates with its outside environment. A PLC program is repeatedly executed in an infinite
loop, for which each iteration is called a scan cycle. Typically each scan cycle can be divided
into three phases:

\begin{enumerate}

\item \textbf{Input phase} during which PLC system reads the values of sensors and
copies them into memory which forms a snapshot of the environment. These values do not change
throughout the rest of the cycle.

\item \textbf{Calculation phase} during which the PLC system
executes the instructions and writes the results into memory. At the beginning of each calculation
phase PLC system does some preparations, such as self-check and timer instructions (for the timers
whose base is 10ms).

\item \textbf{Output phase} during which PLC maps the results into actuators.

\end{enumerate}

There are five standard programming languages for PLC \cite{IEEC61131-3} among which Ladder Diagram
(LD) is the most widely used programming language. We only consider the LD programs in this paper.
As an embedded system, the real-time aspect of PLC system is ensured by the use of
timers.\footnote{Since there are many different kinds of PLCs in the industry and the instructions
used in these PLCs are different from each other, in order to ease the discussion, we focus our
research on S7-200 which is a kind of PLC produced by Siemens. In some cases, time is ensured by
the use of interruptions. We do not consider these cases here.} There are mainly three kinds of
timers in S7-200 \cite{s7-200-manual}: TON-timer, TONR-timer, and TOF-timer. And each timer has
three resolutions. We focus on the 100ms TON-timers. The representation of TON-timer and its
behavior are demonstrated in Fig.\ref{ton_timer}. A TON-timer has two input ports: IN that
indicates whether the timer is enabled and PT that is the preset time of the timer. There are two
output ports: one for the current value and the other for the timer bit. The characteristics of a
TON-timer are informally described as follows : (1)A TON-timer counts time (i.e. increase its
current value) when its IN is ON and it is updated. (2) A TON-timer's timer bit is OFF and current
value is cleared when its IN is OFF. (3) If a TON-timer's current value is greater than or equal to
its PT, its timer bit is ON. (4) A TON-timer continues counting after its PT is reached, and stops
counting when the maximum value 32767 is reached.

\begin{figure}[]
        \center\includegraphics[scale = 0.6]
        {figs/ton_timer}
        \caption{\label{ton_timer} TON timer and its behivour}
      \end{figure}

\subsection{An Illustrative Example}
\label{example}

The program here is used to demonstrate our method and to explain some concepts of LD. A quiz
machine is an equipment used in a contest which involves a host and several players. The host uses
his buttons to start and reset a contest. Every player controls his button which is associated with
a light. The button is used for the player to vie to answer and the light is used to indicate that
the corresponding player get the chance to answer. The LD implementation of quiz machine with three
players and a predefined time of 3 seconds is shown in Fig. \ref{quizmachine}.

A LD program consists of a sequences of rungs. There are 10 rungs in the example program. Each rung
can be seen as a connection between logical relays and coils. For example, the first rung contains
three relays (i.e. $m_1$, $i_1$ and $i_0$) and one coil (i.e. $m_1$). Normally each rung has only
one coil. If a path can be traced between the left side of the rung and the coil, through ON
contacts, the rung is true and the coil storage bit is ON. A normally open contact (-$|~|$-) is
closed when its bit is 1 and it's normally OFF. A normally closed contact (-$|/|$-) is closed when
its coil is 0 and it's normally ON.

Three time related properties should be satisfied. One of the properties concerns the scenario that
: the host presses the reset button and after a while he presses the start button. If no one
presses the button between the time he presses the start button and timeout, the light indicating
timeout will turn on and the other lights stay off. In previous work \cite{cg_Coq_PLCII}, we built
an abstract model of the quiz machine program. The properties were proved to be satisfied by the
model. In this paper, in order to prove the correctness of the abstract model, we first build a
concrete model. Since the abstract model in \cite{cg_Coq_PLCII} is syntactically different from a
timed STS model, we construct another timed STS model then prove they are semantically equivalent.
Finally, we prove there is a refinement relation between the two timed STSs. In section
\ref{modeling_PLC_with_Timers}, we will describe the details.

\begin{figure}[]
        \center\includegraphics[scale = 0.45]
        {figs/quizmachine}
        \caption{\label{quizmachine} The Ladder Diagram of Quiz Machine}
      \end{figure}

\section{The Computation Model and the Refinement Relation}
\label{comp_model_refinement_relation}

Given a set $\mathcal {V}$ of variables, a state $s$ is a type-consistent interpretation of
$\mathcal{V}$. $s(v)$ denotes the value of $v$ at state $s$. The set of all states over $\mathcal
{V}$ is denoted by $\sum$.

We adopt the definition of synchronous transition systems in \cite{Pnueli98translationvalidation}
with some modifications.

\begin{definition}
The following components define a \textbf{synchronous transition system} (STS) $S = (\mathcal{V},
\Theta, \rho)$:
\begin{itemize}

\item $\mathcal{V}$: A finite set of system variables.

\item $\Theta$ : An initial condition predicate over system states.

\item $\rho$ : A transition relation. $\rho$ is a predicate over two states. Given two states $s$ and $s'$,
$\rho(s,s')=true$ iff $s'$ is a possible successor state of $s$.

\end{itemize}

\end{definition}

Before we introduce the additional time-related predicates, we define the timed state sequences.

\begin{definition}

A \textbf{timed state sequence} $\varsigmaup = (\sigma, T)$ consists of an infinite sequence
$\sigma$ of states $\sigma_i \in \sum ~(i \ge 0)$, and an infinite sequence $T$ of corresponding
times $T_i \in N$ that satisfy the following conditions:

\begin{itemize}

\item \textbf{Monotonicity} $\forall i \ge 0$ $T_{i+1} \geq T_i$.

\item \textbf{Progress} $\forall n \in N$, $\exists i \geq 0, T_i > n$.

\end{itemize}

The set of all timed state sequences is denoted by $\varrhoup$.

Alternatively a timed sequence can be represented by a function of type $N \rightarrow (\sum \times
N)$. Intuitively giving the function an index it will output a state and its corresponding time at
the index.
\end{definition}

\begin{definition}

A \textbf{time related predicate} is a predicate of type $\varrhoup \to bool$ that refers to
component $T$ of a timed state sequence.

\end{definition}

In the modeling of PLC programs, the behavior of timers is model by a set of time related
predicates.

An STS together with a set of time related predicates form a computational model.

\begin{definition}

A \textbf{timed synchronous transition system }(timed STS), denoted by TS, is a pair $(S, {\cal
P})$ where $S$ is an STS and ${\cal P}$ is a set of time related predicates.

\end{definition}

Now we give the definition of timed execution sequences of the model.

\begin{definition}

Given an STS $S =(V, \Theta, \rho)$ and an associated timed STS $ST = (S, {\cal P})$ , a timed
execution sequence $\varsigmaup = (\sigma, T)$ of $TS$ is a \textbf{timed state sequence} that
satisfies the following conditions:

\begin{itemize}

\item \textbf{Initiation} : $\Theta(\sigma_0)$ holds.

\item \textbf{Consecution} : $\forall i \in N$, $\rho (\sigma_i,\sigma_{i+1})$ holds.

\item \textbf{Timing Relation} : $\forall p \in {\cal P}$, $p(\varsigmaup)$ holds.

\end{itemize}

The set of all timed execution sequences is denoted by $||TS||$.

\end{definition}

A PLC program can be modeled by a timed STS, since it can be divided into two parts: time-related
part and non-time-related part. The non-time-related part can be modeled by an STS, while the
time-related part can be modeled by a set of predicates. We will describe how to deal with PLC
programs with timers in the section \ref{modeling_PLC_with_Timers}.

The refinement relation of two timed STS is given below based on their timed execution sequences.

\begin{definition}
\label{def_refinement}

Given two timed STSs $A$ and $C$, and two functions $f:N\rightarrow N$ satisfying $\forall i:N,
f(i) < f (i+1)$ and $\phiup : \sum_C \rightarrow \sum_A$, \textbf{{$C$ is a refinement of $A$
relative to $f$ and $\phiup$}} iff $\forall \varsigmaup_C = (\sigma_C, T_C) \in ||C||, \exists
\varsigmaup_A = (\sigma_A, T_A) \in ||A||, \forall i \in N, \phiup(\sigma_C(f(i))) = \sigma_A(i)
\wedge T_C(f(i)) = T_A(i)$.

\end{definition}

\begin{figure}[]
        \center\includegraphics[scale = 0.65]
        {figs/def_refinement}
        \caption{\label{fig_def_refinement} The refinement relation between sequences}
      \end{figure}

Definition \ref{def_refinement} is illustrated graphically in Fig. \ref{fig_def_refinement}.
Intuitively, the function $f$ can be understood as a sampling function. It sets infinite
observation points in the timed execution sequences of system $C$. If $C$ is a refinement of $A$,
then for a sequence $\varsigmaup_C \in ||C||$, the sampled points in $\varsigmaup_C$ forms another
sequence $\varsigmaup_C'$ in which they keeps the same order as $\varsigmaup_C$. By applying
$\phiup$ point-wise to $\varsigmaup_C'$, a new sequence which belongs to $||A||$ can be obtained.

\begin{definition}
\label{def_refinement}

For systems $A$ and $C$, $A$ refines $B$ iff there exists two functions $f$ and $\phiup$ such that
$C$ is a refinement of $A$ relative to $f$ and $\phiup$.
\end{definition}

The problem of checking the correctness of the abstract model turns to a problem of checking
whether there is a refinement relation between abstract model and concrete model.



\section{Modeling and Verification of PLC Programs with Timers}
\label{modeling_PLC_with_Timers}


To model a PLC program, there are several key problems that need to be taken into consideration
 \cite{Mader00aclassification}: (1) how to identify the programming language fragments that are
used; (2) how to model the cyclic operation mode; (3) how to model the timer. Besides these points,
we also investigate the following issues : (1) what are the assumptions and constraints that make
the abstract model correct; (2) how the computation part is model and at what abstract level.
Further more, the computation part can be divided into two sub parts: non-time-related part and
time-related part. In this section, we describe how to get the concrete model mentioned in section
\ref{example} from the PLC program. The abstract model can be obtained based on the concrete model
in the same manner. We first introduce the control flow graph of PLC programs which gives us a
formal base for later discussions.

\subsection{The Structure Representations}
\label{structure_representation}

We first give some definitions about control flow graph (CFG).

\begin{definition}

Let CFG = (V, A) be a directed graph, where $V$ is the set of vertices and $A$ is the set of arcs.
The set $V$ is divided into two subsets $N$ and $E$ such that $N \cap E = \emptyset \wedge N \cup E
= V$. In the graph, vertices in $V$ are represented by cycles while vertices in $E$ are represented
by triangles. An arc that connects two vertices $u$ and $v$ is denoted by $(u,v)$.

CFGs satisfy that $\forall (u,v)\in A, (u\in N \wedge v\in E) \vee (u\in E \wedge v\in N)$.

A \textbf{path} $p = v_1~v_2~\cdots~v_n$ is a sequence of vertices such that $\forall i\in[1,n),
(v_i,v_{i+1})\in A$. For clarity, the vertex $e\in E$ in a path is represented by
``$\stackrel{\underrightarrow{e}}{ }$''. The \textbf{length} of  $p$ is $(n-1)$, denoted by $|p|$.
For all $i\in [1,|p|+1]$, the \textbf{$i$-th element} is denoted by $p_i$.

Vertex $u$ is \textbf{reachable} from vertex $v$ iff there is a path from $u$ to $v$ in the CFG.

For a set $O\subseteq E$, two vertices $v_1,v_2\in O$ are called \textbf{adjacent relative to $O$
and path $p$}, denoted by $adj(v_1, v_2, p, O)$, iff $v_1 = p_1 \wedge v_2 = p_{|p|+1} \wedge
(p-\{v1, v2\}) \cap O = \emptyset$. If $O$ is clear in the context, $O$ will be omitted in
expressions.

\end{definition}

Take the CFG $(c)$ in Fig. \ref{cfg_quiz_mechine} for example. If $O = \{e_1,e_3,e_5\}$, then $e_1$
and $e_5$ are not adjacent relative to path $\stackrel{\underrightarrow{e_1}}{ } v_1
\stackrel{\underrightarrow{e_2}}{ } v_2 \stackrel{\underrightarrow{e_3}}{ } v_3
\stackrel{\underrightarrow{e_4}}{ } v_4 \stackrel{\underrightarrow{e_5}}{ }$, since $e_3\in O$ is
in the path. $e_1$ and $e_3$ are adjacent relative to path $\stackrel{\underrightarrow{e_1}}{ } v_1
\stackrel{\underrightarrow{e_2}}{ } v_2 \stackrel{\underrightarrow{e_3}}{ } $.



The control structure of a PLC program can be described by a CFG $g = ((N,E), A)$. Intuitively
vertices in $N$ are used to represent rungs in PLC programs and vertices in $E$ are used to
represent the observation points. As mentioned in section \ref{PLC_TIMERS}, each scan cycle
contains an input phase and an output phase. Hence, there are always two vertices in the CFG: one
is $v_i$ representing the input phase and the other is $v_o$ representing the output phase. For all
$v$ such that $(v,v_i)\in A$ is \textbf{input related}. A vertex is \textbf{timer related} if the
rung it represents is a timer instruction.

For instance, the CFG of the quiz machine program is the CFG $(c)$ in Fig. \ref{cfg_quiz_mechine}.
Vertex $v_0$ represents the preparation at the beginning of the calculation phase. Each of the rest
vertices (except $v_o$ and $v_i$) denotes a rung in the program. Since there is no loop and branch
constructs in the calculation phase, the CFG is a simple cycle (Note the cyclic behavior of PLC).
Every vertex $v$ is associated with three sets:  $ref_v$, $def_v$, and $times_v$, where $ref_v$ is
the set of variables vertex $v$ refers to, $def_v$ is the set of variables vertex $v$ defines (or
may modify) and $times_v$ is the set of all possible time spans used to reach vertex $v$ from the
beginning of the calculation phase. Comparing to other variables, their values can change multiple
times without explicit assignments. Hence, in the associated table a timer bit can occur in
different $def$ sets. CFG and the table form a formal representation of a PLC program's control
structure.

\begin{figure}[]
        \center\includegraphics[scale = 0.86]
        {figs/cfg_quiz_mechine}
        \caption{\label{cfg_quiz_mechine} The CFG of the quiz machine program}
      \end{figure}

\subsection{Modeling PLC Programs}
\label{model_plc_programs}

The timed STS can be constructed based on either the PLC program or an existing timed STS. The
model on which the construction is based is called base model. A timed STS is associated with a
CFG. Comparing to the CFG of the PLC program, CFGs of the timed STSs are abstract. The CFG
associated to the base model is denoted by $g=((N,E),A)$ and $V = (N,E)$. The primed version of
variables and notations belong to the model under constructions. For example, $g'=((N',E'),A')$ is
used to represent the CFG associated to the model we are building. There are two points we need to
mention before we introduce the principles of building timed STSs:

\begin{itemize}

\item The consecution condition of the timed STS is a disjunction composed of a set of
clauses. Both the disjunction and the clauses are predicates over two states.

\item Each vertex in set $N$ of a CFG is associated with some computations. Its predecessors
(successors, resp.) can be understood as the points where we can observe the input (output, resp.)
values of the computations. Furthermore, these computations are represented by several clauses in
the disjunction.

\end{itemize}

\subsubsection{Selecting Observation Vertices}

According to $g$, we need to select several observation points, i.e., a set $O\subseteq N$. These
points can be understood as the sampling points. $O$ should satisfy the condition that there is no
loop between any two adjacent vertices in $O$, i.e., $\forall e_1~e_2 \in
O,|\{p|~adj(e_1,e_2,p)\}|$ is finite ($|\bullet|$ is the number of elements in $\bullet$). $g'$ can
be constructed based on $g$ and $O$. There is correspondence between $g$ and $g'$, which is denoted
by an relation $\alpha \subseteq V\times V'$. The associated table is calculated based on $\alpha$.
For all $v'\in V'$, if $v' \in N$, then $def'_{v'} = \bigcup_{(v,v')\in\alpha} def_v \bigwedge
ref'_{v'} = \bigcup_{(v,v')\in\alpha} ref_v \bigwedge times'_{v'} =
MIN_{(v,v')\in\alpha}(times_v)$. If vertex $v$ is timer (input,  resp.) related, then for each $v'$
such that $(v, v')\in\alpha$ is also timer (input,  resp.) related. For instance, assume the base
CFG is $(c)$ in Fig. \ref{cfg_quiz_mechine}. For the concrete model, we choose $O=
\{e_1,e_2,\cdots,e_{11}\}$. Then the abstract CFG $(b)$ is obtained. The $\alpha$ between $(c)$ and
$(b)$ is
$\{(v_o,v_0'),(v_i,v_0'),(v_0,v_0'),(v_1,v_1'),(v_2,v_2'),(v_3,\\v_3'),(v_4,v_4'),(v_5,v_5'),
(v_6,v_6'),(v_7,v_7'),(v_8,v_8'),(v_9,v_9'),(v_{10},v_{10}'),(e_{10},e_{11}'),(e_{12},e_{11}'),(e_{11},
e_{11}'\\),(e_1,e_1'),(e_2,e_2'),(e_3,e_3'),
(e_4,e_4'),(e_5,e_5'),(e_6,e_6'),(e_7,e_7'),(e_8,e_8'),(e_9,e_9'),(e_{10},e_{10}')\}$. Since
$e_{12}$ is input related, $e'_{11}$ is input related.


The set $O$ and $\alpha$ can be used to build the link between the base model and the new model. In
other words, the sampling function $f$ can be constructed based on them.

\subsubsection{Variables}

According to $O$, we have the definition of $location$ in which each element corresponds to an
observation vertex. A timed execution sequence is a sequence of states. The index of the sequence
which means the total number of observation vertices visited before the position is of type
$position$. The type of variables is $Position\to Prop$. Variable of type $program\_counter$ is
used to record the observation vertex at the current position The notion of time is introduced by
type $Time\_c$. Function $fc$ maps each position to a time and it satisfies the monotonic property.

{\small
\begin{verbatim}
Inductive location : Set :=
  e11 | e1 | e2 | e3 | e4 | e5 | e6 | e7 | e8 | e9 | e10.
Definition Position := nat.
Definition Var_c := Position -> Prop.
Definition program_counter := Position -> location.
Definition Time_c := nat.
Variable fc : Position -> Time_c.
Hypothesis fc_monotonic : forall p, fc p < fc (S p).
\end{verbatim}
}

Then, we have the following definitions of variables. The system state consists of 16 variables :
$i_0,i_1,i_2,i_3,i_4,m_1,m_2,m_3,m_4,m_5,o_0,o_1,o_2,o_3,t_1$ and $pc$.

{\small
\begin{verbatim}
Variables i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 t1: Var_c.
Variable pc : program_counter.
\end{verbatim}
}


\subsubsection{Non-Time-Related Part}

Based on base CFG and the operational semantics of PLC, the non-time-related part of the program
can be modeled by an STS. An STS consists of two parts : initiation condition $\Theta$ and
consecution condition $\rho$. $\rho$ is a disjunction. Each clause in the disjunction is a
predicate over two states. The problem of constructing the STS is then turned into the problem of
finding the clauses in the disjunction. Informally in CFG the computations along the path
connecting any two adjacent observation vertices is modeled by a clause in the disjunction. A
clause is also a predicate over two states. An informal clause generation algorithm can be
described as: for all $p~ (v_1~v_2 \in O)$ such that $adj(v_1,v_2,p)$, build a clause.

$\Theta$ and $\rho$ of the concrete model are as follows. There are 11 clauses in $\rho$, since the
number of tuples $(v_1,v_2,p)$ such that $v_1~v_2\in O$ and $adj(v_1,v_2,p)$ is 11. In order to
save space, notation $V = \{i_0, i_1, i_2, i_3, i_4, m_1, m_2, m_3, m_4, m_5, o_0, o_1, o_2, o_3,
t_1\}$ and $pres(U)=\bigwedge_{v\in U}(v' = v)$ are used in the following expressions. $pres(U)$
means all variables in $U$ do not change their values.


{\small
\begin{verbatim}
Definition initial_condition_c
  i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 pc t1:=
    ~i0/\~i1/\~i2/\~i3/\~i4/\~m1/\~m2/\~m3/\~m4/\~m5/\
    ~o0/\~o1/\~o2/\~o3/\pc=e11/\~t1.
Definition next_condition_c
  (i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3:Prop) l
  (t1 i0' i1' i2' i3' i4' m1' m2' m3' m4' m5' o0' o1' o2' o3':Prop)l' t1':=
  match l with
     e11 => l' =e1/\pres(V\{i0,i1,i2,i3,l})
    |e1 => m1'=((m1\/i0)/\(~i1))/\l'=e2/\pres(V\{m1,l})
    |e2 => l' =e3/\pres(V\{t1,l})
    |e3 => m2'=((m2\/(~t1/\i2/\~m5))/\m1)/\l'=e4/\pres(V\{m2,l})
    |e4 => m3'=((m3\/(~t1/\i3/\~m5))/\m1)/\l'=e5/\pres(V\{m3,l})
    |e5 => m4'=((m4\/(~t1/\i4/\~m5))/\m1)/\l'=e6/\pres(V\{m4,l})
    |e6 => m5'=((m2\/m3\/m4\/m5)/\m1)/\l'=e7/\pres(V\{m5,l})
    |e7 => o1'=m2/\l'=e8/\pres(V\{o1,l})
    |e8 => o2'=m3/\l'=e9/\pres(V\{o2,l})
    |e9 => o3'=m4/\l'=e10/\pres(V\{o3,l})
    |e10=> o0'=(t1/\~m5)/\l'=e11/\pres(V\{o0,l})
  end.
Hypothesis initial_states_c : initial_condition_c
  (i0 0) (i1 0) (i2 0) (i3 0) (i4 0) (m1 0) (m2 0) (m3 0) (m4 0)
  (m5 0) (o0 0) (o1 0) (o2 0) (o3 0) (pc 0) (t1 0).
Hypothesis next_states_c : forall p,
  next_condition_c (i0 p)(i1 p)(i2 p)(i3 p)(i4 p)(m1 p)(m2 p)(m3 p)(m4 p)
   (m5 p)(o0 p)(o1 p)(o2 p)(o3 p)(pc p)(t1 p)(i0 (S p))(i1 (S p))(i2 (S p))
   (i3 (S p))(i4 (S p))(m1 (S p))(m2 (S p))(m3 (S p))(m4 (S p))(m5 (S p))
   (o0 (S p))(o1 (S p))(o2 (S p))(o3 (S p))(pc (S p))(t1 (S p)).
\end{verbatim}
}

\subsubsection{Time-Related Part}

Particularly the time-related part is the activities of timers. As discussed in
\cite{cg_Coq_PLCII}, a TON-timer is modeled by three hypotheses that constitute the time related
predicates part of the timed STS:
\begin{itemize}

\item \textbf{(Reset)}. If the IN to the timer turns off, so does the timer bit.

\item \textbf{(Set)}. If the preset time period is passed and that the IN has been
kept ON during this period, then the timer bit will turn ON.

\item \textbf{(Set Reverse)}. If the timer bit turns ON, then its IN must have been
kept ON for a period larger than the preset time.

\end{itemize}

For the concrete model, we have the following three hypotheses:

\begin{itemize}

\item \textbf{Reset}. If the timer instruction is executed at position $p$ and the timer's IN is
OFF at position $p$, then the timer bit will turn OFF at next position.


{\small
\begin{verbatim}
Hypothesis h_t1_reset_c : forall p, pc p=e2 -> ~m1 p -> ~t1 (S p).
\end{verbatim}
}

\item \textbf{Set}. Given two positions $p_1$ and $p_2$ at which the timer instruction is executed.
If the time interval between them is greater than or equal to $t1_PT_c$ which is the preset time of
the timer, as well as its $IN$ keeps ON during this period, then the timer bit will turn ON at next
position. {\small
\begin{verbatim}
Hypothesis h_t1_set_c : forall p1 p2, pc p1 = e2 -> pc p2 = e2 ->
  t1_PT_c <= fc p2 - fc p1 -> being_true_c m1 p1 p2 e2 pc->t1(S p2).
\end{verbatim}
}

\item \textbf{Set Reverse}. If the timer bit is ON at position $p_2$ and the timer instruction was
executed at the previous position, then there exists a position $p_1$ before $p_2$ such that the
time interval between $pred~p_1$ and $p_2$ is great than or equal to $t1_PT_c$ and during this
period its IN stays ON. {\small
\begin{verbatim}
Hypothesis h_t1_true_c : forall p2, pc (pred p2) = e2 -> t1 p2 ->
  exists p1, pc p1 = e2 /\ t1_PT_c <= fc (pred p2) - fc p1 /\
    being_true_c m1 p1 (pred p2) e2 pc.
\end{verbatim}
}
\end{itemize}

Finally we have the timed STS for the concrete model. The timed STS of the abstract model is built
on the concrete model with $O=\{e'_{11}\}$. We omit the equivalent proof here.

{\small
\begin{verbatim}
Definition initial_condition_a
  i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 t1:=
  ~i0 /\ ~i1 /\ ~i2 /\ ~i3 /\ ~i4 /\ ~m1 /\ ~m2 /\
  ~m3 /\ ~m4 /\ ~m5 /\ ~o0 /\ ~o1 /\ ~o2 /\ ~o3 /\ ~t1.
Definition next_condition_a
(i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 t1 i0' i1' i2' i3' i4'
  m1' m2' m3' m4' m5' o0' o1' o2' o3' t1' : Prop) :=
    (m1' = ((i0' \/ m1) /\ ~ i1')) /\
    (m2' = (((~ t1' /\ i2' /\ ~ m5) \/ m2) /\ m1')) /\
    (m3' = (((~ t1' /\ i3' /\ ~ m5) \/ m3) /\ m1')) /\
    (m4' = (((~ t1' /\ i4' /\ ~ m5) \/ m4) /\ m1')) /\
    (m5' = (((m2' \/ m3' \/ m4') \/ m5) /\ m1')) /\
    (o1' = m2')/\(o2' = m3')/\(o3' = m4') /\(o0' = (t1' /\ ~ m5')).
Hypothesis initial_states_a:initial_condition_a
  (i0 0) (i1 0) (i2 0) (i3 0) (i4 0) (m1 0) (m2 0) (m3 0)
  (m4 0) (m5 0) (o0 0) (o1 0) (o2 0) (o3 0) (t1 0).
Hypothesis next_states_a:forall p,next_condition_a(i0 p)(i1 p)(i2 p)(i3 p)(i4 p)
  (m1 p)(m2 p)(m3 p)(m4 p)(m5 p)(o0 p)(o1 p)(o2 p)(o3 p)(t1 p)(i0(S p))
  (i1(S p))(i2(S p))(i3(S p))(i4(S p))(m1(S p))(m2(S p))(m3(S p))
  (m4(S p))(m5(S p))(o0(S p))(o1(S p))(o2(S p))(o3(S p))(t1(S p)).
Hypothesis h_t1_reset : forall c, ~ m1 c -> ~ t1 c.
Hypothesis h_t1_set :
  forall c1 c2,t1_PT<=f(pred c2)-f(pred c1)->being_true m1 c1 c2->t1 c2.
Hypothesis h_t1_true :
  forall c2,t1 c2->exists c1,t1_PT<=f(pred c2)-f(pred c1)/\being_true m1 c1 c2.
\end{verbatim}
}


\subsection{Outline of Refinement Proof}
\label{outline_proof}

Given two timed STSs $A$ and $C$ such that $A$ is built on $C$. $C$ is a refinement of $A$ iff the
sampled version of a sequence which belongs to $||C||$ also belongs to $||A||$. Based on the
structure of timed STS, the refinement proof can be done structurally. Suppose we want to prove the
refinement relation between the concrete and abstract models, we can take the following steps.

\subsubsection{Define Functions}

Define two functions: sampling function $f : N\rightarrow N$ and mapping function $\phiup : \sum_C
\rightarrow \sum_A$. In the example $\phiup$ is an identical function, since the variables used at
concrete and abstract models are the same. Because the observation vertex is only $e'_{11}$, $f$ is
defined as follows. Predicate $P$ is the condition under which sampling operation can happen. Based
on the definition of $f\_mapping$, four important properties of $f\_mapping$ are proved. The
sampled sequence is obtained with the help of $abs$. For instance, the sampled sequence of $m_1$ is
denoted by $(abs~ m_1)$.

{\small
\begin{verbatim}
Definition P x := pc x = l11.
Definition f_mapping_0_to_Prop (x:nat)(P:nat->Prop) :=
  (forall x', x' < x -> ~ P x') /\ P x.
Definition f_mapping_0_to := epsilon nat_non_empty (f_mapping_0_to_Prop P).
Definition f_mapping_S_n_to_Prop (n x:nat)(P:nat->Prop) :=
  (forall x', n < x' < x -> ~ P x') /\ P x /\ (n < x).
Definition f_mapping_S_n_to(n:nat):=
  epsilon nat_non_empty(f_mapping_S_n_to_Prop n P).
Fixpoint f_mapping (n : nat) := match n with
    0 => f_mapping_0_to
  | S p => f_mapping_S_n_to (f_mapping p)
end.
Lemma f_mapping_before_0 : forall p, p < f_mapping 0 -> ~ P p.
Lemma f_mapping_point_to_e11 : forall n, P (f_mapping n).
Lemma f_mapping_no_e11_between:forall n p,f_mapping n<p<f_mapping(S n)->~P p.
Lemma f_mapping_monotony_Sn: forall n, f_mapping n < f_mapping (S n).

Definition abs (T:Type)(v : Var_c)(n:nat):= v (f_mapping n).
\end{verbatim}
}

\subsubsection{Cyclic Behavior Mode}

The cyclic behavior of a timed STS $ST$ is ensured by showing the fact that for all $\varsigmaup
\in ||ST||$ there exists a input related vertex which is visited infinitely in $\varsigmaup$. For
the concrete model lemma $f\_mapping\_point\_to\_e11$ shows that along any $\varsigmaup \in ||ST||$
$e_{11}$ which is input related is visited infinitely.


\subsubsection{Prove that the Sampled Sequence Satisfies Initiation Condition of $||A||$}

Given a timed state sequence $\varsigmaup_C$ of $C$, we need to prove that $\varsigmaup_A =
\phiup\circ\varsigmaup_C\circ f$ is a sequence satisfying $\Theta_A(proj_1(\varsigmaup_A(0))$.
$proj_1$ is a function to get the first element of a pair. The proof of the theorem depends on the
initiation and consecution conditions of $||C||$. Usually, the theorem is not difficult to prove.
For the example, we prove the following theorem.

{\small
\begin{verbatim}
Theorem concrete_trace_sat_abs_init_condition: initial_condition_a (abs i0 0)
 (abs i1 0)(abs i2 0)(abs i3 0)(abs i4 0)(abs m1 0)(abs m2 0)(abs m3 0)
 (abs m4 0)(abs m5 0)(abs o0 0)(abs o1 0)(abs o2 0)(abs o3 0)(abs t1 0).
\end{verbatim}
}

\subsubsection{Prove the Sampled Sequence Satisfies Consecution Condition of $||A||$}

Given a timed state sequence $\varsigmaup_C$ of $C$, we need to prove that $\varsigmaup_A =
\phiup\circ\varsigmaup_C\circ f$ is a sequence satisfying $\forall i \in N$, $\rho_A
(proj_1(\varsigmaup(i),proj_1(\varsigmaup(i+1))$. The theorem about the consecution is stated
below. To prove the theorem, based on the construction of the abstract timed STS, it is enough to
prove that $\forall (s_1~s_2\cdots s_m : \sum_C)(e_1~e_m \in O)(p =
\stackrel{\underrightarrow{e_1}}{ }v_1 \stackrel{\underrightarrow{e_2}}{ } \cdots v_{m-1}
\stackrel{\underrightarrow{e_m}}{ }), adj(e_1,e_2,p) \wedge (\forall i\in[1,m),c_i (s_i s_{i+1}))
\to disj_a (s_1~s_m)$ where $c_i$ is the clauses associated with $v_i$ and $disj_a$ is the
disjunction representing the consecution condition. This property can be verified by a model
checker or an automatic first order theorem prover.

{\small
\begin{verbatim}
Theorem concrete_trace_sat_abs_next_condition : forall p, next_condition_a
  (abs i0 p)(abs i1 p)(abs i2 p)(abs i3 p)(abs i4 p)(abs m1 p)(abs m2 p)
  (abs m3 p)(abs m4 p)(abs m5 p)(abs o0 p)(abs o1 p)(abs o2 p)(abs o3 p)
  (abs t1 p)(abs i0 (S p))(abs i1 (S p))(abs i2 (S p))(abs i3 (S p))
  (abs i4 (S p))(abs m1 (S p))(abs m2 (S p))(abs m3 (S p))(abs m4 (S p))
  (abs m5 (S p))(abs o0 (S p))(abs o1 (S p))(abs o2 (S p))(abs o3 (S p))
  (abs t1 (S p)).
\end{verbatim}
}


\subsubsection{State the Constraints}
\label{lab_constraints}

The PLC programs considered in this paper are programs without loops, i.e., if we remove vertices
$v_i$, $v_o$ and their associated arcs, the rest CFG is an acyclic directed graph.



For each timer, there is an accompanying set of constraints. We assume there is only one timer $t$
in the program. For programs with multiple timers, the constraints are the union of the constraints
of each timer.

\begin{itemize}

\item $\forall (e_1~ e_m \in O) ~(p = \stackrel{\underrightarrow{e_1}}{ }v_1 \stackrel{\underrightarrow{e_2}}{
} \cdots v_{m-1} \stackrel{\underrightarrow{e_m}}{ }), adj(e_1, e_m, p) \wedge (\exists i, (1 \le i
< m) \wedge t \in def_{v_i}) \rightarrow (\exists! i, (1 \le i < m) \wedge t \in def_{v_i})$. This
formula describes that if $e_1$ and $e_m$ are adjacent relative to $p$ then the timer bit of $t$
can change at most once along path $p$ and changes at the same vertex in $p$.

\item $\forall (e_1~ e_m \in O) (1\le i < m)(p = \stackrel{\underrightarrow{e_1}}{ }v_1 \stackrel{\underrightarrow{e_2}}{
} \cdots v_{m-1} \stackrel{\underrightarrow{e_m}}{ }))~(p' = \stackrel{\underrightarrow{e_1}}{
}v_1' \stackrel{\underrightarrow{e_2'}}{ } \cdots v_{m-1}' \stackrel{\underrightarrow{e_m}}{ })),
adj(e_1, e_m, p)  \wedge (t \in def_{v_i})\rightarrow (\forall j, 1 < j < i \rightarrow e_j =
e_j')$. This formula describes that if $v_1$ and $v_m$ are adjacent relative to $p$ and $p'$ and
$v_i$ is the time instruction, then the sub-paths in $p$ and $p'$ that connect $e_1$ and $e_i$ are
the same.

\item $\forall (e_1~ e_m \in O)(1\le i < m)(p = \stackrel{\underrightarrow{e_1}}{ }v_1 \stackrel{\underrightarrow{e_2}}{
} \cdots v_{m-1} \stackrel{\underrightarrow{e_m}}{ }), adj(e_1, e_m, p) \wedge (t \in def_{v_i})
\rightarrow ((\forall j, i \le j < m \rightarrow ref(IN_t) \cap def_{v_j} = \emptyset) \vee
(\forall j, 1 \le j \le i \rightarrow ref(IN_t) \cap def_{v_j} = \emptyset))$. This formula
describes that the timer instruction is executed at vertex $i$ and the variables used in the timer
instruction doesn't change either from vertex $v_i$ to vertex $e_m$ or from vertex $e_1$ to $v_i$
in path $p$. $ref(IN_t)$ is the set of variables used to calculate IN of $t$. For example, in Fig.
\ref{quizmachine} $ref(IN_{t_1})=\{m_1\}$.

\end{itemize}

The constraints are used to prove the correctness of the model under construction based on the base
model. Informally, for any two adjacent vertices $v_1,v_m \in O$ that have a timer related vertex
$v_i$ between them (depicted in Fig. \ref{fig_constraints}), the values used by the timer
instruction are sampled at $e_i$ and the output of the instruction can be observed at $e_{i+1}$.
The constraints ensure that (1) the values used by the timer instruction stay the same from $e_1$
and $e_i$ or from $e_i$ to $e_n$; (2) the time interval from $e_1$ to $e_i$ is always the same; (3)
the timer bit value changes only at $v_i$. In the abstract model, the computations between $e_1$
and $e_n$ are abstracted and represented by a single vertex $v'_2$. The constraints make the values
used or output by the timer instruction visible at $e'_1$ or $e'_2$.

\begin{figure}[]
        \center\includegraphics[scale = 0.93]
        {figs/fig_constraints}
        \caption{\label{fig_constraints} The use of Constraints}
      \end{figure}

The following lemmas about the constraints of $t_1$ show that along the path
$\stackrel{\underrightarrow{e''_{11}}}{ } v'_0 \stackrel{\underrightarrow{e'_1}}{ } v_1 \cdots
\stackrel{\underrightarrow{e_{10}}}{ } v'_{10} \stackrel{\underrightarrow{e'_{11}}}{ }$, (1) the
value of timer bit changes only at $v'_2$, that is to say the values of timer bit at $'e_3$ and
$e'_{11}$ are the same; (2) the value of $m_1$ (i.e. the value of the timer's IN) stays the same
between $e'_2$ and $e'_{11}$.

{\small
\begin{verbatim}
Definition offset := 2.
Definition t1_loc := e2.
Lemma t1_loc_change_property:forall n p1 p2,p1=f_mapping n->p2=f_mapping(S n)->
  (forall p, p1 <= p < p2 -> pc p <>  t1_loc -> t1 (S p) = t1 p).
Lemma offset_is_t1_loc : forall n p1 p2,p1=f_mapping n ->
  p2 = f_mapping(S n)-> pc (offset + p1) = t1_loc.
Lemma offset_is_less : forall n p1 p2, p1 = f_mapping n ->
  p2 = f_mapping (S n) -> offset  < p2 - p1.
Lemma t1_loc_is_unique:forall n p1 p2, p1=f_mapping n->p2=f_mapping(S n)->
  forall p, p1 <= p < p2 -> p <> offset + p1 -> pc p <> t1_loc.
Lemma offset_change_property:forall n p1 p2,p1=f_mapping n->p2=f_mapping(S n)->
  forall p, offset + p1 <= p < p2 -> m1 (S p) = m1 p.
\end{verbatim}
}

\subsubsection{Prove the Sampled Sequence Satisfies the Time Related Predicate of $||A||$}

This proof of this result is done based on the theorems describing constraints and time related
predicates of $||A||$. If we prove the theorems directly on the concrete model, a lot of irrelevant
information will be introduced which makes the proof much more difficult. The theorems about the
constraints can help to remove the irrelevant information. In practice, they are useful. The
following theorems are about the timed related predicates and are similar to those hypotheses of
the abstract model except that each variable is replaced by its abstract version. They are proved
based on the theorems of constraints and timed related predicates of the concrete model.

{\small
\begin{verbatim}
Theorem concrete_trace_sat_abs_t1_reset:forall c, ~abs m1  c->~abs t1
Theorem concrete_trace_sat_abs_t1_true :
  forall c2,abs t1  c2->exists c1, t1_PT <= abs fc (pred c2)
  - abs fc (pred c1) /\ being_true (abs m1) c1 c2.
Theorem concrete_trace_sat_abs_t1_set :
  forall c1 c2, t1_PT <= abs fc  (pred c2)-abs fc (pred c1)->
    being_true (abs m1) c1 c2 -> abs t1 c2.
\end{verbatim}
}



\subsubsection{The Final Theorem}

The final result is that for all properties that are held by the abstract model are also held by
the concrete model which is stated as the following theorem. In the theorem $P$ is a property of
the abstract model and sequences of form ``$abs~\bullet$'' are the sampled sequences. By using this
theorem, the properties we have proved in \cite{cg_Coq_PLCII} are also satisfied by the concrete
model.

{\small
\begin{verbatim} Theorem refinement_relation_property :
 forall P (f:Cycle->Time)(i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 t1:Var),
  (initial_condition_a(i0 0)(i1 0)(i2 0)(i3 0)(i4 0)(m1 0)(m2 0)(m3 0)(m4 0)
    (m5 0)(o0 0)(o1 0)(o2 0)(o3 0)(t1 0)) ->
  (forall p : Cycle,next_condition_a (i0 p)(i1 p)(i2 p)(i3 p)(i4 p)(m1 p)
    (m2 p)(m3 p)(m4 p)(m5 p)(o0 p)(o1 p)(o2 p)(o3 p)(t1 p)(i0(S p))(i1(S p))
    (i2(S p))(i3(S p))(i4(S p))(m1(S p))(m2(S p))(m3(S p))(m4(S p))(m5(S p))
    (o0(S p))(o1(S p))(o2(S p))(o3(S p))(t1(S p))) ->
  (forall c,~m1 c->~t1 c)->(forall c1 c2,t1_PT<=f(pred c2)-f(pred c1) ->
    being_true m1 c1 c2 -> t1 c2) ->
  (forall c2,t1 c2->exists c1,t1_PT<=f(pred c2)-f(pred c1)/\being_true m1 c1 c2)->
  P i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 t1) ->
  P(abs i0)(abs i1)(abs i2)(abs i3)(abs i4)(abs m1)(abs m2)(abs m3)(abs m4)
   (abs m5)(abs o0)(abs o1)(abs o2)(abs o3)(abs t1).
\end{verbatim}
}

\subsubsection{Remarks}

After analyze the dependence among theorems used in the proof, it can be concluded that the proof
of the refinement relation between abstract and concrete time related predicates only uses the
theorem of constraints and concrete timed related predicates, which means that the refinement
relation between abstract and concrete models are independent of the STS of the concrete model if
the concrete model satisfies the constraints. By modifying the source codes or generating codes
that satisfy the constraints, the refinement relation between the time related parts is held
without proving.

\section{Conclusions}
\label{conclusion}

In this paper, we continue our work of modeling and verification of PLC programs. In our previous
work, a formalization of TON-timers of PLC programs was presented in the theorem proving system
Coq. The behavior of a timer was characterized by a set of axioms at an abstract level. The work
has two key aspects. One is that we build an abstract model of a PLC program. The other is how to
interpret the abstract model based on the concrete model. In this paper, we extend our previous
work. Firstly, a concrete model is built and the correctness of the abstract model is proved based
on the concrete model. Secondly, the interpretation is generalized by the notion of mapping
function. Both works are done in a unified framework. The essence of the framework is the notion of
refinement relation. We also give the outline of the correctness proof. As a case study, we
reconsider the quiz machine program. The experiment result show the correctness of the framework.
This framework also allow us to build models hierarchically that still keep the refinement
relation. Our future work is to study how to get a more abstract model based on a given property.
The use of refinement relation between the concrete model and the abstract model benefits us in at
least two ways: First, it facilitates the modeling and verification of the PLC source codes. Since
all properties which are held by the abstract model are also satisfied by the concrete model, it is
sufficient to do the verification at the abstract level which is relatively simpler; Second, in the
code generation process, the refinement relation can be used in two directions: (1) the correctness
of the implementation can be checked according to the relation; (2) the constraints learnt from the
building process of refinement relation can be deployed to direct the code generation process by
adding certain constraints.




\bibliographystyle{splncs}
\bibliography{ref}

\end{document}
